$\forall$${\it es}$:ES, ${\it Sys}$:AbsInterface(Top), $f$:sys{-}antecedent(${\it es}$;${\it Sys}$), $x$, $y$:E(${\it Sys}$).
\\[0ex]$x$ is $f$$\ast$($y$) $\Rightarrow$ (loc($x$) = loc($y$) $\in$ Id) $\Rightarrow$ $x$ $\leq$loc $y$